SherbyNet - /page/wikibook/entry.mu

Micron Document

<!DOCTYPE html>

<title>Guarded Command Language</title>

</head>

<span id="openzim-page-title" class="mw-page-title-main"><span class="mw-page-title-main">Guarded Command Language</span></span>

</h1>

</header>

<p>The <b>Guarded Command Language</b> (<b>GCL</b>) is a <a href="Programming_language" title="Programming language">programming language</a> defined by <a href="Edsger_Dijkstra" class="mw-redirect" title="Edsger Dijkstra">Edsger Dijkstra</a> for <a href="Predicate_transformer_semantics" title="Predicate transformer semantics">predicate transformer semantics</a> in EWD472.<sup id="cite_ref-EWD472_1-0" class="reference"><a href="#cite_note-EWD472-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup> It combines programming concepts in a compact way. It makes it easier to develop a program and its proof hand-in-hand, with the proof ideas leading the way; moreover, parts of a program can actually be <i>calculated</i>.

</p><p>An important property of <b>GCL</b> is <a href="Nondeterministic_programming" title="Nondeterministic programming">nondeterminism</a>. For example, in the if-statement, several alternatives may be true, and the choice is made at runtime, when the if-statement is executed. This frees the programmer from having to make unnecessary choices and is an aid in the formal development of programs.

</p><p><b>GCL</b> includes the multiple assignment statement. For example, execution of the statement <code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">x, y:= y, x</code> is done by first evaluating the righthand side values and then storing them in the lefthand variables. Thus, this statement swaps the values of <style data-mw-deduplicate="TemplateStyles:r886049734">

/* start https://en.wikipedia.org/ */

.mw-parser-output .monospaced{font-family:monospace,monospace}

/* end https://en.wikipedia.org/ */

</style><span class="monospaced">x</span> and <span class="monospaced">y</span>.

</p><p>The following books discuss the development of programs using <b>GCL</b>:

</p>

/* start https://en.wikipedia.org/ */

.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}

/* end https://en.wikipedia.org/ */

</style><cite class="citation book cs1"><a href="Edsger_W._Dijkstra" title="Edsger W. Dijkstra">Dijkstra, Edsger W.</a> (1976). <span class="id-lock-registration" title="Free registration required"><a rel="nofollow" class="external text" href="https://archive.org/details/disciplineofprog0000dijk"><i>A Discipline of Programming</i></a></span>. Prentice Hall. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0132158718</bdi>.</cite></li>

<li><cite id="CITEREFGries1981" class="citation book cs1 cs1-prop-foreign-lang-source cs1-prop-foreign-lang-source cs1-prop-foreign-lang-source cs1-prop-foreign-lang-source cs1-prop-foreign-lang-source"><a href="David_Gries" title="David Gries">Gries, D.</a> (1981). <a rel="nofollow" class="external text" href="https://link.springer.com/book/10.1007/978-1-4612-5983-1"><i>The Science of Programming</i></a>. Monographs in Computer Science (in English, Spanish, Japanese, Chinese, Italian, and Russian). New York: Springer Verlag. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-1-4612-5983-1">10.1007/978-1-4612-5983-1</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0-387-96480-5</bdi>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:37034126">37034126</a>.</cite></li>

<li><cite id="CITEREFDijkstraFeijen1988" class="citation book cs1"><a href="Edsger_W._Dijkstra" title="Edsger W. Dijkstra">Dijkstra, Edsger W.</a>; Feijen, Wim H.J. (1988). <a rel="nofollow" class="external text" href="https://dl.acm.org/doi/book/10.5555/576038"><i>A Method of Programming</i></a>. Boston, MA: Addison-Wesley Longman Publishing Co., Inc. p. 200. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0-201-17536-3</bdi>.</cite></li>

<li><cite id="CITEREFKaldewaij1990" class="citation book cs1">Kaldewaij, Anne (1990). <a rel="nofollow" class="external text" href="https://dl.acm.org/doi/10.5555/98158"><i>Programming: the derivation of algorithms</i></a>. Prentice-Hall, Inc. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0132041081</bdi>.</cite></li>

<li><cite id="CITEREFCohen1990" class="citation book cs1">Cohen, Edward (1990). <a href="David_Gries" title="David Gries">David Gries</a> (ed.). <a rel="nofollow" class="external text" href="https://link.springer.com/book/10.1007/978-1-4613-9706-9"><i>Programming in the 1990s: An introduction to the calculation of programs</i></a>. Texts and Monographs in Computer Science. Springer Verlag. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-1-4613-9706-9">10.1007/978-1-4613-9706-9</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-1-4613-9706-9</bdi>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:1509875">1509875</a>.</cite></li></ul>

<p><br>

</p>

<div class="mw-heading mw-heading2"><h2 id="Guarded_command">Guarded command</h2></div>

<p>A guarded command consists of a boolean condition or <a href="Guard_(computer_science)" title="Guard (computer science)">guard</a>, and a statement "guarded" by it. The statement is only executed if the guard is true, so when reasoning about the statement, the condition can be assumed true. This makes it easier to prove the <a href="Computer_program" title="Computer program">program</a> meets a <a href="Program_specification" class="mw-redirect" title="Program specification">specification</a>.

</p>

<div class="mw-heading mw-heading3"><h3 id="Syntax"><a href="Syntax_(programming_languages)" title="Syntax (programming languages)">Syntax</a></h3></div>

<p>A guarded command is a <a href="Statement_(programming)" class="mw-redirect" title="Statement (programming)">statement</a> of the form G → S, where

</p>

<ul><li>G is a <a href="Proposition" title="Proposition">proposition</a>, called the guard</li>

<li>S is a statement</li></ul>

<div class="mw-heading mw-heading3"><h3 id="Semantics"><a href="Semantics" title="Semantics">Semantics</a></h3></div>

<ul><li>If G evaluates to true, S is eligible to be executed. In most GCL constructs, multiple guarded commands may have guards that are true, and exactly one of them is chosen <i>arbitrarily</i> to be executed.</li>

<li>If G is false, S will not be executed.</li></ul>

<div class="mw-heading mw-heading2"><h2 id="skip_and_abort">skip and abort</h2></div>

<p><b>skip</b> and <b>abort</b> are important statements in the guarded command language. <b>abort</b> is the undefined instruction: do anything. It does not even need to terminate. It is used to describe the program when formulating a proof, in which case the proof usually fails. <b>skip</b> is the empty instruction: do nothing. It is often used when the syntax requires a statement but the <a href="State_(computer_science)" title="State (computer science)">state</a> should not change.

</p>

<div class="mw-heading mw-heading3"><h3 id="Syntax_2">Syntax</h3></div>

</pre>

<pre><b>abort</b>

</pre>

<div class="mw-heading mw-heading3"><h3 id="Semantics_2">Semantics</h3></div>

<ul><li><b>skip</b>: do nothing</li>

<li><b>abort</b>: do anything</li></ul>

<div class="mw-heading mw-heading2"><h2 id="Assignment"><a href="Assignment_(computer_programming)" class="mw-redirect" title="Assignment (computer programming)">Assignment</a></h2></div>

<p>Assigns values to <a href="Variable_(programming)" class="mw-redirect" title="Variable (programming)">variables</a>.

</p>

<div class="mw-heading mw-heading3"><h3 id="Syntax_3">Syntax</h3></div>

<pre>v := E

</pre>

<p>or

</p>

</pre>

<p>where

</p>

<ul><li>v are program variables</li>

<li>E are expressions of the same <a href="Data_type" title="Data type">data type</a> as their corresponding variables</li></ul>

<div class="mw-heading mw-heading2"><h2 id="Catenation">Catenation</h2></div>

<p>Statements are separated by one semicolon (;)

</p>

<div class="mw-heading mw-heading2"><h2 id="Selection:_if"><a href="Conditional_(programming)" class="mw-redirect" title="Conditional (programming)">Selection</a>: if</h2></div>

<p>The selection (often called the "conditional statement" or "if statement") is a list of guarded commands, of which one is chosen to execute. If more than one guard is true, one statement whose guard is true is arbitrarily chosen to be executed. If no guard is true, the result is undefined, that is, equivalent to <b>abort</b>. Because at least one of the guards must be true, the empty statement <b>skip</b> is often needed. The statement <b>if fi</b> has no guarded commands, so there is never a true guard. Hence, <b>if fi</b> is equivalent to <b>abort</b>.

</p>

<div class="mw-heading mw-heading3"><h3 id="Syntax_4">Syntax</h3></div>

<pre><b>if</b> G0 → S0

□ G1 → S1

...

□ Gn → Sn

</pre>

<div class="mw-heading mw-heading3"><h3 id="Semantics_3">Semantics</h3></div>

<p>Upon execution of a selection, the guards are evaluated. If none of the guards is <i>true</i>, then the selection aborts, otherwise one of the clauses with a <i>true</i> guard is chosen arbitrarily and its statement is executed.

</p>

<div class="mw-heading mw-heading3"><h3 id="Implementation">Implementation</h3></div>

<p>GCL does not specify an implementation. Since guards cannot have <a href="Side_effect_(computer_science)" title="Side effect (computer science)">side effects</a> and the choice of clause is arbitrary, an implementation may evaluate the guards in any sequence and choose the first <i>true</i> clause, for example.

</p>

<div class="mw-heading mw-heading3"><h3 id="Examples">Examples</h3></div>

<div class="mw-heading mw-heading4"><h4 id="Simple">Simple</h4></div>

<p>In <a href="Pseudocode" title="Pseudocode">pseudocode</a>:

</p>

<pre>if a < b then set c to True

else set c to False

</pre>

<p>In guarded command language:

</p>

<pre><b>if</b> a > b → c := true

□ a < b → c := false

</pre>

<p>In pseudocode:

</p>

<pre>if error is True then set x to 0

</pre>

<p>In guarded command language:

</p>

<pre><b>if</b> error → x := 0

□ <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \neg }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \neg }</annotation>

</semantics>

</math></span><img src="./fa78fd02085d39aa58c9e47a6d4033ce41e02fad.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: 0.204ex; margin-bottom: -0.376ex; width:1.55ex; height:1.176ex;" alt="{\displaystyle \neg }" loading="lazy"></span>error → <b>skip</b>

</pre>

<p>If the second guard is omitted and error is False, the result is abort.

</p>

<div class="mw-heading mw-heading4"><h4 id="More_guards_true">More guards true</h4></div>

<pre><b>if</b> a ≥ b → max := a

□ b ≥ a → max := b

</pre>

<p>If a = b, either a or b is chosen as the new value for the maximum, with equal results. However, the <a href="Implementation" title="Implementation">implementation</a> may find that one is easier or faster than the other. Since there is no difference to the programmer, any implementation will do.

</p>

<div class="mw-heading mw-heading2"><h2 id="Repetition:_do"><a href="Control_flow#Loops" title="Control flow">Repetition</a>: <i>do</i></h2></div>

<p>Execution of this repetition, or loop, is shown below.

</p>

<div class="mw-heading mw-heading3"><h3 id="Syntax_5">Syntax</h3></div>

<pre><b>do</b> G0 → S0

□ G1 → S1

...

□ Gn → Sn

</pre>

<div class="mw-heading mw-heading3"><h3 id="Semantics_4">Semantics</h3></div>

<p>Execution of the repetition consists of executing 0 or more <i>iterations</i>, where an iteration consists of arbitrarily choosing a guarded command <span class="texhtml">Gi → Si</span> whose guard <span class="texhtml">Gi</span> is true and executing the command <span class="texhtml">Si</span>. Thus, if all guards are initially false, the repetition terminates immediately, without executing an iteration. Execution of the repetition <b>do od</b>, which has no guarded commands, executes 0 iterations, so <b>do od</b> is equivalent to <b>skip</b>.

</p>

<div class="mw-heading mw-heading3"><h3 id="Examples_2">Examples</h3></div>

<div class="mw-heading mw-heading4"><h4 id="Original_Euclidean_algorithm">Original <a href="Euclidean_algorithm" title="Euclidean algorithm">Euclidean algorithm</a></h4></div>

<pre>a, b := A, B;

<b>do</b> a < b → b := b - a

□ b < a → a := a - b

</pre>

<p>This repetition ends when a = b, in which case a and b hold the <a href="Greatest_common_divisor" title="Greatest common divisor">greatest common divisor</a> of A and B.

</p><p>Dijkstra sees in this algorithm a way of synchronizing two infinite cycles <code>a := a - b</code> and <code>b := b - a</code> in such a way that <code>a≥0</code> and <code>b≥0</code> remains true.

</p>

<div class="mw-heading mw-heading4"><h4 id="Extended_Euclidean_algorithm"><a href="Extended_Euclidean_algorithm" title="Extended Euclidean algorithm">Extended Euclidean algorithm</a></h4></div>

<pre>a, b, x, y, u, v := A, B, 1, 0, 0, 1;

<b>do</b> b ≠ 0 →

q, r := a <b>div</b> b, a <b>mod</b> b;

a, b, x, y, u, v := b, r, u, v, x - q*u, y - q*v

</pre>

<p>This repetition ends when b = 0, in which case the variables hold the solution to <a href="B%C3%A9zout's_identity" title="Bézout's identity">Bézout's identity</a>: xA + yB = gcd(A,B) .

</p>

<div class="mw-heading mw-heading4"><h4 id="Non-deterministic_sort">Non-deterministic sort</h4></div>

<pre><b>do</b> a<b → a, b := b, a

□ b<c → b, c := c, b

□ c<d → c, d := d, c

</pre>

<p>The program keeps on permuting elements while one of them is greater than its successor. This non-deterministic <a href="Bubble_sort" title="Bubble sort">bubble sort</a> is not more efficient than its deterministic version, but easier to prove: it will not stop while the elements are not sorted and that each step it sorts at least 2 elements.

</p>

<pre>x, y = 1, 1;

<b>do</b> x≠n →

<b>if</b> f(x) ≤ f(y) → x := x+1

□ f(x) ≥ f(y) → y := x; x := x+1

</pre>

<p>This algorithm finds the value 1 ≤ <i>y</i> ≤ <i>n</i> for which a given integer function <i>f</i> is maximal. Not only the computation but also the final state is not necessarily uniquely determined.

</p>

<div class="mw-heading mw-heading2"><h2 id="Applications">Applications</h2></div>

<div class="mw-heading mw-heading3"><h3 id="Programs_correct_by_construction">Programs correct by construction</h3></div>

<p>Generalizing the observational <a href="Congruence_relation" title="Congruence relation">congruence</a> of Guarded Commands into a <a href="Lattice_(order)" title="Lattice (order)">lattice</a> has led to <a href="Refinement_Calculus" class="mw-redirect" title="Refinement Calculus">Refinement Calculus</a>.<sup id="cite_ref-2" class="reference"><a href="#cite_note-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup> This has been mechanized in <a href="Formal_Methods" class="mw-redirect" title="Formal Methods">Formal Methods</a> like <a href="B-Method" title="B-Method">B-Method</a> that allow one to formally derive programs from their specifications.

</p>

<div class="mw-heading mw-heading3"><h3 id="Asynchronous_circuits">Asynchronous circuits</h3></div>

<p>Guarded commands are suitable for <a href="Quasi-delay-insensitive_circuit" title="Quasi-delay-insensitive circuit">quasi-delay-insensitive circuit</a> design because the repetition

allows arbitrary relative delays for the selection of different commands. In this application,

a logic gate driving a node <i>y</i> in the circuit consists of two guarded commands, as follows:

</p>

<pre>PullDownGuard → y := 0

PullUpGuard → y := 1

</pre>

<p><i>PullDownGuard</i> and <i>PullUpGuard</i> here are functions of the logic gate's inputs,

which describe when the gate pulls the output down or up, respectively. Unlike classical

circuit evaluation models, the repetition for a set of guarded commands (corresponding to an asynchronous circuit) can accurately describe all possible dynamic behaviors of that circuit.

Depending on the model one is willing to live with for the electrical circuit elements,

additional restrictions on the guarded commands may be necessary for a guarded-command description

to be entirely satisfactory. Common restrictions include stability, non-interference, and absence

of self-invalidating commands.<sup id="cite_ref-synthesis_tr_3-0" class="reference"><a href="#cite_note-synthesis_tr-3"><span class="cite-bracket">[</span>3<span class="cite-bracket">]</span></a></sup> AI

</p>

<div class="mw-heading mw-heading3"><h3 id="Model_checking">Model checking</h3></div>

<p>Guarded commands are used within the <a href="Promela" title="Promela">Promela</a> programming language, which is used by the <a href="SPIN_model_checker" title="SPIN model checker">SPIN model checker</a>. SPIN verifies correct operation of concurrent software applications.

</p>

<div class="mw-heading mw-heading3"><h3 id="Other">Other</h3></div>

<p>The Perl module <a rel="nofollow" class="external text" href="https://metacpan.org/module/Commands::Guarded">Commands::Guarded</a> implements a deterministic, rectifying variant on Dijkstra's guarded commands.

</p>

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

<li id="cite_note-EWD472-1"><span class="mw-cite-backlink"><b><a href="#cite_ref-EWD472_1-0">^</a></b></span> <span class="reference-text"><cite id="CITEREFDijkstra" class="citation web cs1"><a href="E._W._Dijkstra" class="mw-redirect" title="E. W. Dijkstra">Dijkstra, Edsger W</a>. <a rel="nofollow" class="external text" href="http://www.cs.utexas.edu/users/EWD/ewd04xx/EWD472.PDF">"EWD472: Guarded commands, non-determinacy and formal. derivation of programs"</a> <span class="cs1-format">(PDF)</span><span class="reference-accessdate">. Retrieved <span class="nowrap">August 16,</span> 2006</span>.</cite></span>

</li>

<li id="cite_note-2"><span class="mw-cite-backlink"><b><a href="#cite_ref-2">^</a></b></span> <span class="reference-text"><cite id="CITEREFBack1978" class="citation web cs1"><a href="Ralph-Johan_Back" title="Ralph-Johan Back">Back, Ralph J</a> (1978). <a rel="nofollow" class="external text" href="https://web.archive.org/web/20110720175255/http://crest.abo.fi/publications/public/1978/OnTheCorrectnessOfRefinementStepsInProgramDevelpmentTR.pdf">"On the Correctness of Refinement Steps in Program Development (Phd-Thesis)"</a> <span class="cs1-format">(PDF)</span>. Archived from <a rel="nofollow" class="external text" href="http://crest.abo.fi/publications/public/1978/OnTheCorrectnessOfRefinementStepsInProgramDevelpmentTR.pdf">the original</a> <span class="cs1-format">(PDF)</span> on 2011-07-20.</cite></span>

</li>

<li id="cite_note-synthesis_tr-3"><span class="mw-cite-backlink"><b><a href="#cite_ref-synthesis_tr_3-0">^</a></b></span> <span class="reference-text"><cite id="CITEREFMartin" class="citation web cs1">Martin, WILLIAM. <a rel="nofollow" class="external text" href="http://resolver.caltech.edu/CaltechCSTR:1991.cs-tr-93-28">"Synthesis of Asynchronous VLSI Circuits"</a>.</cite></span>

</li>

</ol></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .hlist dl,.mw-parser-output .hlist ol,.mw-parser-output .hlist ul{margin:0;padding:0}.mw-parser-output .hlist dd,.mw-parser-output .hlist dt,.mw-parser-output .hlist li{margin:0;display:inline}.mw-parser-output .hlist.inline,.mw-parser-output .hlist.inline dl,.mw-parser-output .hlist.inline ol,.mw-parser-output .hlist.inline ul,.mw-parser-output .hlist dl dl,.mw-parser-output .hlist dl ol,.mw-parser-output .hlist dl ul,.mw-parser-output .hlist ol dl,.mw-parser-output .hlist ol ol,.mw-parser-output .hlist ol ul,.mw-parser-output .hlist ul dl,.mw-parser-output .hlist ul ol,.mw-parser-output .hlist ul ul{display:inline}.mw-parser-output .hlist .mw-empty-li{display:none}.mw-parser-output .hlist dt::after{content:": "}.mw-parser-output .hlist dd::after,.mw-parser-output .hlist li::after{content:" · ";font-weight:bold}.mw-parser-output .hlist dd:last-child::after,.mw-parser-output .hlist dt:last-child::after,.mw-parser-output .hlist li:last-child::after{content:none}.mw-parser-output .hlist dd dd:first-child::before,.mw-parser-output .hlist dd dt:first-child::before,.mw-parser-output .hlist dd li:first-child::before,.mw-parser-output .hlist dt dd:first-child::before,.mw-parser-output .hlist dt dt:first-child::before,.mw-parser-output .hlist dt li:first-child::before,.mw-parser-output .hlist li dd:first-child::before,.mw-parser-output .hlist li dt:first-child::before,.mw-parser-output .hlist li li:first-child::before{content:" (";font-weight:normal}.mw-parser-output .hlist dd dd:last-child::after,.mw-parser-output .hlist dd dt:last-child::after,.mw-parser-output .hlist dd li:last-child::after,.mw-parser-output .hlist dt dd:last-child::after,.mw-parser-output .hlist dt dt:last-child::after,.mw-parser-output .hlist dt li:last-child::after,.mw-parser-output .hlist li dd:last-child::after,.mw-parser-output .hlist li dt:last-child::after,.mw-parser-output .hlist li li:last-child::after{content:")";font-weight:normal}.mw-parser-output .hlist ol{counter-reset:listitem}.mw-parser-output .hlist ol>li{counter-increment:listitem}.mw-parser-output .hlist ol>li::before{content:" "counter(listitem)"\a0 "}.mw-parser-output .hlist dd ol>li:first-child::before,.mw-parser-output .hlist dt ol>li:first-child::before,.mw-parser-output .hlist li ol>li:first-child::before{content:" ("counter(listitem)"\a0 "}

/* end https://en.wikipedia.org/ */

</style><style data-mw-deduplicate="TemplateStyles:r1126788409">

/* start https://en.wikipedia.org/ */

.mw-parser-output .plainlist ol,.mw-parser-output .plainlist ul{line-height:inherit;list-style:none;margin:0;padding:0}.mw-parser-output .plainlist ol li,.mw-parser-output .plainlist ul li{margin-bottom:0}

/* end https://en.wikipedia.org/ */

</style><style data-mw-deduplicate="TemplateStyles:r1236075235">

/* start https://en.wikipedia.org/ */

.mw-parser-output .navbox{box-sizing:border-box;border:1px solid #a2a9b1;width:100%;clear:both;font-size:88%;text-align:center;padding:1px;margin:1em auto 0}.mw-parser-output .navbox .navbox{margin-top:0}.mw-parser-output .navbox+.navbox,.mw-parser-output .navbox+.navbox-styles+.navbox{margin-top:-1px}.mw-parser-output .navbox-inner,.mw-parser-output .navbox-subgroup{width:100%}.mw-parser-output .navbox-group,.mw-parser-output .navbox-title,.mw-parser-output .navbox-abovebelow{padding:0.25em 1em;line-height:1.5em;text-align:center}.mw-parser-output .navbox-group{white-space:nowrap;text-align:right}.mw-parser-output .navbox,.mw-parser-output .navbox-subgroup{background-color:#fdfdfd}.mw-parser-output .navbox-list{line-height:1.5em;border-color:#fdfdfd}.mw-parser-output .navbox-list-with-group{text-align:left;border-left-width:2px;border-left-style:solid}.mw-parser-output tr+tr>.navbox-abovebelow,.mw-parser-output tr+tr>.navbox-group,.mw-parser-output tr+tr>.navbox-image,.mw-parser-output tr+tr>.navbox-list{border-top:2px solid #fdfdfd}.mw-parser-output .navbox-title{background-color:#ccf}.mw-parser-output .navbox-abovebelow,.mw-parser-output .navbox-group,.mw-parser-output .navbox-subgroup .navbox-title{background-color:#ddf}.mw-parser-output .navbox-subgroup .navbox-group,.mw-parser-output .navbox-subgroup .navbox-abovebelow{background-color:#e6e6ff}.mw-parser-output .navbox-even{background-color:#f7f7f7}.mw-parser-output .navbox-odd{background-color:transparent}.mw-parser-output .navbox .hlist td dl,.mw-parser-output .navbox .hlist td ol,.mw-parser-output .navbox .hlist td ul,.mw-parser-output .navbox td.hlist dl,.mw-parser-output .navbox td.hlist ol,.mw-parser-output .navbox td.hlist ul{padding:0.125em 0}.mw-parser-output .navbox .navbar{display:block;font-size:100%}.mw-parser-output .navbox-title .navbar{float:left;text-align:left;margin-right:0.5em}body.skin--responsive .mw-parser-output .navbox-image img{max-width:none!important}@media print{body.ns-0 .mw-parser-output .navbox{display:none!important}}

/* end https://en.wikipedia.org/ */

</style></div><div role="navigation" class="navbox" aria-labelledby="Edsger_Dijkstra318" style="padding:3px"><table class="nowraplinks mw-collapsible autocollapse navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="3"><style data-mw-deduplicate="TemplateStyles:r1239400231">

/* start https://en.wikipedia.org/ */

.mw-parser-output .navbar{display:inline;font-size:88%;font-weight:normal}.mw-parser-output .navbar-collapse{float:left;text-align:left}.mw-parser-output .navbar-boxtext{word-spacing:0}.mw-parser-output .navbar ul{display:inline-block;white-space:nowrap;line-height:inherit}.mw-parser-output .navbar-brackets::before{margin-right:-0.125em;content:"[ "}.mw-parser-output .navbar-brackets::after{margin-left:-0.125em;content:" ]"}.mw-parser-output .navbar li{word-spacing:-0.125em}.mw-parser-output .navbar a>span,.mw-parser-output .navbar a>abbr{text-decoration:inherit}.mw-parser-output .navbar-mini abbr{font-variant:small-caps;border-bottom:none;text-decoration:none;cursor:inherit}.mw-parser-output .navbar-ct-full{font-size:114%;margin:0 7em}.mw-parser-output .navbar-ct-mini{font-size:114%;margin:0 4em}html.skin-theme-clientpref-night .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}@media(prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}}@media print{.mw-parser-output .navbar{display:none!important}}

/* end https://en.wikipedia.org/ */

</style><div id="Edsger_Dijkstra318" style="font-size:114%;margin:0 4em"><a href="Edsger_W._Dijkstra" title="Edsger W. Dijkstra">Edsger Dijkstra</a></div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%">Works</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><i>A Primer of ALGOL 60 Programming</i> (book)</li>

<li><i>Structured Programming</i> (book)</li>

<li><i>A Discipline of Programming</i> (book)</li>

<li><i>A Method of Programming</i> (book)</li>

<li><i>Predicate Calculus and Program Semantics</i> (book)</li>

<li><i>Selected Writings on Computing: A Personal Perspective</i> (book)</li>

<li><i>A Note on Two Problems in Connexion with Graphs</i></li>

<li><i>Cooperating Sequential Processes</i></li>

<li><i>Solution of a Problem in Concurrent Programming Control</i></li>

<li><i>The Structure of the 'THE'-Multiprogramming System</i></li>

<li><i><a href="Go_To_Statement_Considered_Harmful" class="mw-redirect" title="Go To Statement Considered Harmful">Go To Statement Considered Harmful</a></i></li>

<li><i>Notes on Structured Programming</i></li>

<li><i>The Humble Programmer</i></li>

<li><i>Programming Considered as a Human Activity</i></li>

<li><i>How Do We Tell Truths That Might Hurt?</i></li>

<li><i>On the Role of Scientific Thought</i></li>

<li><i>Self-stabilizing Systems in Spite of Distributed Control</i></li>

<li><i><a href="On_the_Cruelty_of_Really_Teaching_Computer_Science" title="On the Cruelty of Really Teaching Computer Science">On the Cruelty of Really Teaching Computer Science</a></i></li>

<li><a href="Edsger_W._Dijkstra#Selected_publications" title="Edsger W. Dijkstra">Selected papers</a></li>

<li><a href="EWDs" class="mw-redirect" title="EWDs">EWD manuscripts</a></li></ul>

</div></td><td class="noviewer navbox-image" rowspan="3" style="width:1px;padding:0 0 0 2px"><div><span typeof="mw:File"></span></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Computer_science#Areas_of_computer_science" title="Computer science">Main research<br>areas</a></th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Theoretical_computer_science" title="Theoretical computer science">Theoretical computing science</a></li>

<li><a href="Software_engineering" title="Software engineering">Software engineering</a></li>

<li><a href="Systems_science" title="Systems science">Systems science</a></li>

<li><a href="Algorithm_design" class="mw-redirect" title="Algorithm design">Algorithm design</a> (<a href="Dijkstra's_algorithm" title="Dijkstra's algorithm">Dijkstra's algorithm</a>)</li>

<li><a href="Concurrent_computing" title="Concurrent computing">Concurrent computing</a></li>

<li><a href="Distributed_computing" title="Distributed computing">Distributed computing</a></li>

<li><a href="Formal_methods" title="Formal methods">Formal methods</a></li>

<li><a href="Programming_methodology" class="mw-redirect" title="Programming methodology">Programming methodology</a></li>

<li><a href="Programming_language_research" class="mw-redirect" title="Programming language research">Programming language research</a></li>

<li><a href="Software_design" title="Software design">Program design</a> and <a href="Software_development" title="Software development">development</a></li>

<li><a href="Software_architecture" title="Software architecture">Software architecture</a></li>

<li><a href="Philosophy_of_computer_science" title="Philosophy of computer science">Philosophy of computer programming and computing science</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Related<br>people</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Shlomi_Dolev" title="Shlomi Dolev">Shlomi Dolev</a></li>

<li><a href="Per_Brinch_Hansen" title="Per Brinch Hansen">Per Brinch Hansen</a></li>

<li><a href="Tony_Hoare" title="Tony Hoare">Tony Hoare</a></li>

<li><a href="Ole-Johan_Dahl" title="Ole-Johan Dahl">Ole-Johan Dahl</a></li>

<li><a href="Leslie_Lamport" title="Leslie Lamport">Leslie Lamport</a></li>

<li><a href="David_Parnas" title="David Parnas">David Parnas</a></li>

<li><a href="Jaap_A._Zonneveld" title="Jaap A. Zonneveld">Jaap A. Zonneveld</a></li>

<li><a href="Carel_S._Scholten" title="Carel S. Scholten">Carel S. Scholten</a></li>

<li><a href="Adriaan_van_Wijngaarden" title="Adriaan van Wijngaarden">Adriaan van Wijngaarden</a></li>

<li><a href="Niklaus_Wirth" title="Niklaus Wirth">Niklaus Wirth</a></li></ul>

</div></td></tr><tr><td class="navbox-abovebelow plainlist" colspan="3"><div>

<ul><li><span class="noviewer" typeof="mw:File"><span title="Wikiquote page"></span></span> <a href="https://en.wikiquote.org/wiki/Special:Search/Edsger_W._Dijkstra" class="extiw external" title="wikiquote:Special:Search/Edsger W. Dijkstra"><b>Wikiquote</b></a></li></ul>

</div></td></tr></tbody></table></div></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2025-04-28" href="https://en.wikipedia.org/wiki/?title=Guarded_Command_Language&oldid=1287811651">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>